#!/usr/bin/ruby -w

require "rubygems"
require "treetop"
Treetop.load("sat_grammar")

# Define relevant classes
class BinaryNode
  attr_reader(:left, :right)

  def initialize(left, right)
    @left = left
    @right = right
  end
end

class Or < BinaryNode
  def to_s
    return @left.to_s + " v " + @right.to_s
  end
end

class And < BinaryNode
  def to_s
    return @left.to_s + " ^ " + @right.to_s
  end
end

class Literal
  attr_reader(:value)

  def initialize(value)
    @value = value
  end

  def to_s
    return @value.to_s
  end
end

class NegationLiteral < Literal
  def to_s
    return "!" + @value.to_s
  end
end

def sat_parse(formula)
  parser = SatParser.new
  ast = parser.parse(formula)
  if ast
    puts "Successfully parsed formula: " + formula
    return sat_tree_maker(ast)
  else
    puts "Failed to parse formula: " + formula
  end
end

def sat_tree_maker(ast)
  puts "Processing: " + ast.text_value

  # Formula
  if ast.text_value[0..0] == "(" then
    puts "Formula:" + ast.elements[2].text_value
    return sat_tree_maker(ast.elements[2])

  # And operation
  elsif ast.text_value[0..0] == "*" then
    puts "And operation: " + ast.text_value
    #return And.new()

  # Or operation
  elsif ast.text_value[0..0] == "+" then
    puts "Or operation: " + ast.text_value
    #return Or.new()

  # Literal
  elsif ast.text_value.to_i >= 1 then
    puts "Literal: " + ast.text_value
    return Literal.new(ast.text_value.to_i)

  # Negation literal
  elsif ast.text_value[0..0] == "-" then
    puts "Negation literal:" + ast.text_value
    return NegationLiteral.new(ast.text_value.to_i)
  end
end

# Tests to see if the grammar works
sat_parse("(1 2)")
sat_parse("-(1 2)")
sat_parse("(+(1 +(1 2)))")
sat_parse("(-1)")
sat_parse("(+(1 2))")
sat_parse("(+(1 +(1 2)))")
sat_parse("(*(+(-1) +(2 3)))")
